Left Termination of the query pattern
query(g)
w.r.t. the given Prolog program could successfully be proven:

(0) Obligation:

Clauses:

append(nil, XS, XS).
append(cons(X, XS), YS, cons(X, ZS)) :- append(XS, YS, ZS).
reverse(nil, nil).
reverse(cons(X, nil), cons(X, nil)).
reverse(cons(X, XS), YS) :- ','(reverse(XS, ZS), append(ZS, cons(X, nil), YS)).
shuffle(nil, nil).
shuffle(cons(X, XS), cons(X, YS)) :- ','(reverse(XS, ZS), shuffle(ZS, YS)).
query(XS) :- shuffle(cons(X, XS), YS).

Query: query(g)

(1) PrologToDTProblemTransformerProof (SOUND transformation)

Built DT problem from termination graph DT10.

digraph dp_graph {
node [outthreshold=100, inthreshold=100];
1 [label="D: query(T1)\n\nT1 is ground", fontsize=16, style=filled, fillcolor=lightyellow, color=red];
2 [label="2: query(T1), SCOPE: 1, CLAUSE: 7\n\nT1 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
3 [label="3: shuffle(cons(X3, T3), X4)\n\nT3 is ground\nX3 is free\nX4 is free", fontsize=16, style=filled, fillcolor=lightyellow];
4 [label="4: shuffle(cons(X3, T3), X4), SCOPE: 2, CLAUSE: 5 | shuffle(cons(X3, T3), X4), SCOPE: 2, CLAUSE: 6\n\nT3 is ground\nX3 is free\nX4 is free", fontsize=16, style=filled, fillcolor=lightyellow];
5 [label="5: shuffle(cons(X3, T3), X4), SCOPE: 2, CLAUSE: 6\n\nT3 is ground\nX3 is free\nX4 is free", fontsize=16, style=filled, fillcolor=lightyellow];
6 [label="C: ','(reverse(T6, X19), shuffle(X19, X21))\n\nT6 is ground\nX21 is free\nX19 is free", fontsize=16, style=filled, fillcolor=lightyellow];
7 [label="A: reverse(T6, X19)\n\nT6 is ground\nX19 is free", fontsize=16, style=filled, fillcolor=lightyellow];
8 [label="8: shuffle(T7, X21)\n\nT7 is ground\nX21 is free", fontsize=16, style=filled, fillcolor=lightyellow];
9 [label="9: reverse(T6, X19), SCOPE: 3, CLAUSE: 2 | reverse(T6, X19), SCOPE: 3, CLAUSE: 3 | reverse(T6, X19), SCOPE: 3, CLAUSE: 4\n\nT6 is ground\nX19 is free", fontsize=16, style=filled, fillcolor=lightyellow];
10 [label="10: reverse(T6, X19), SCOPE: 3, CLAUSE: 2\n\nT6 is ground\nX19 is free", fontsize=16, style=filled, fillcolor=lightyellow];
11 [label="11: reverse(T6, X19), SCOPE: 3, CLAUSE: 3 | reverse(T6, X19), SCOPE: 3, CLAUSE: 4\n\nT6 is ground\nX19 is free", fontsize=16, style=filled, fillcolor=lightyellow];
12 [label="12: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
13 [label="13: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
14 [label="14: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
15 [label="15: reverse(T6, X19), SCOPE: 3, CLAUSE: 3\n\nT6 is ground\nX19 is free", fontsize=16, style=filled, fillcolor=lightyellow];
16 [label="16: reverse(T6, X19), SCOPE: 3, CLAUSE: 4\n\nT6 is ground\nX19 is free", fontsize=16, style=filled, fillcolor=lightyellow];
17 [label="17: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
18 [label="18: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
19 [label="19: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
20 [label="20: ','(reverse(T18, X39), append(X39, cons(T17, nil), X40))\n\nT17 is ground\nT18 is ground\nX40 is free\nX39 is free", fontsize=16, style=filled, fillcolor=lightyellow];
21 [label="21: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
22 [label="22: reverse(T18, X39)\n\nT18 is ground\nX39 is free", fontsize=16, style=filled, fillcolor=lightyellow];
23 [label="B: append(T19, cons(T17, nil), X40)\n\nT17 is ground\nT19 is ground\nX40 is free", fontsize=16, style=filled, fillcolor=lightyellow];
24 [label="24: append(T19, cons(T17, nil), X40), SCOPE: 4, CLAUSE: 0 | append(T19, cons(T17, nil), X40), SCOPE: 4, CLAUSE: 1\n\nT17 is ground\nT19 is ground\nX40 is free", fontsize=16, style=filled, fillcolor=lightyellow];
25 [label="25: append(T19, cons(T17, nil), X40), SCOPE: 4, CLAUSE: 0\n\nT17 is ground\nT19 is ground\nX40 is free", fontsize=16, style=filled, fillcolor=lightyellow];
26 [label="26: append(T19, cons(T17, nil), X40), SCOPE: 4, CLAUSE: 1\n\nT17 is ground\nT19 is ground\nX40 is free", fontsize=16, style=filled, fillcolor=lightyellow];
27 [label="27: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
28 [label="28: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
29 [label="29: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
30 [label="30: append(T34, cons(T35, nil), X62)\n\nT34 is ground\nT35 is ground\nX62 is free", fontsize=16, style=filled, fillcolor=lightyellow];
31 [label="31: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
32 [label="32: shuffle(T7, X21), SCOPE: 5, CLAUSE: 5 | shuffle(T7, X21), SCOPE: 5, CLAUSE: 6\n\nT7 is ground\nX21 is free", fontsize=16, style=filled, fillcolor=lightyellow];
33 [label="33: shuffle(T7, X21), SCOPE: 5, CLAUSE: 5\n\nT7 is ground\nX21 is free", fontsize=16, style=filled, fillcolor=lightyellow];
34 [label="34: shuffle(T7, X21), SCOPE: 5, CLAUSE: 6\n\nT7 is ground\nX21 is free", fontsize=16, style=filled, fillcolor=lightyellow];
35 [label="35: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
36 [label="36: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
37 [label="37: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
38 [label="38: ','(reverse(T43, X77), shuffle(X77, X78))\n\nT43 is ground\nX78 is free\nX77 is free", fontsize=16, style=filled, fillcolor=lightyellow];
39 [label="39: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
40 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
1 -> 40 [arrowhead = none ];
40 -> 2;

41 [label="ONLY EVAL with clause\nquery(X2) :- shuffle(cons(X3, X2), X4).\nand substitutionT1 -> T3,\nX2 -> T3", fontsize=14, style = filled, fillcolor = lightblue];
2 -> 41 [arrowhead = none ];
41 -> 3;

42 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
3 -> 42 [arrowhead = none ];
42 -> 4;

43 [label="BACKTRACK\nfor clause: shuffle(nil, nil)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
4 -> 43 [arrowhead = none ];
43 -> 5;

44 [label="ONLY EVAL with clause\nshuffle(cons(X16, X17), cons(X16, X18)) :- ','(reverse(X17, X19), shuffle(X19, X18)).\nand substitutionX3 -> X20,\nX16 -> X20,\nT3 -> T6,\nX17 -> T6,\nX18 -> X21,\nX4 -> cons(X20, X21)", fontsize=14, style = filled, fillcolor = lightblue];
5 -> 44 [arrowhead = none ];
44 -> 6;

45 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
6 -> 45 [arrowhead = none ];
45 -> 7;

46 [label="SPLIT 2\nnew knowledge:\nT6 is ground\nT7 is ground\nreplacements:X19 -> T7", fontsize=14, style = filled, fillcolor = violet];
6 -> 46 [arrowhead = none ];
46 -> 8;

47 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
7 -> 47 [arrowhead = none ];
47 -> 9;

48 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
8 -> 48 [arrowhead = none ];
48 -> 32;

49 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
9 -> 49 [arrowhead = none ];
49 -> 10;

50 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
9 -> 50 [arrowhead = none ];
50 -> 11;

51 [label="EVAL with clause\nreverse(nil, nil).\nand substitutionT6 -> nil,\nX19 -> nil", fontsize=14, style = filled, fillcolor = lightblue];
10 -> 51 [arrowhead = none ];
51 -> 12;

52 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
10 -> 52 [arrowhead = none ];
52 -> 13;

53 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
11 -> 53 [arrowhead = none ];
53 -> 15;

54 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
11 -> 54 [arrowhead = none ];
54 -> 16;

55 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
12 -> 55 [arrowhead = none ];
55 -> 14;

56 [label="EVAL with clause\nreverse(cons(X26, nil), cons(X26, nil)).\nand substitutionX26 -> T12,\nT6 -> cons(T12, nil),\nX19 -> cons(T12, nil)", fontsize=14, style = filled, fillcolor = lightblue];
15 -> 56 [arrowhead = none ];
56 -> 17;

57 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
15 -> 57 [arrowhead = none ];
57 -> 18;

58 [label="EVAL with clause\nreverse(cons(X36, X37), X38) :- ','(reverse(X37, X39), append(X39, cons(X36, nil), X38)).\nand substitutionX36 -> T17,\nX37 -> T18,\nT6 -> cons(T17, T18),\nX19 -> X40,\nX38 -> X40", fontsize=14, style = filled, fillcolor = lightblue];
16 -> 58 [arrowhead = none ];
58 -> 20;

59 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
16 -> 59 [arrowhead = none ];
59 -> 21;

60 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
17 -> 60 [arrowhead = none ];
60 -> 19;

61 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
20 -> 61 [arrowhead = none ];
61 -> 22;

62 [label="SPLIT 2\nnew knowledge:\nT18 is ground\nT19 is ground\nreplacements:X39 -> T19", fontsize=14, style = filled, fillcolor = violet];
20 -> 62 [arrowhead = none ];
62 -> 23;

63 [label="INSTANCE with matching:\nT6 -> T18\nX19 -> X39", fontsize=14, style = filled, fillcolor = lightgrey];
22 -> 63 [arrowhead = none , style=dashed];
63 -> 7[style=dashed];

64 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
23 -> 64 [arrowhead = none ];
64 -> 24;

65 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
24 -> 65 [arrowhead = none ];
65 -> 25;

66 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
24 -> 66 [arrowhead = none ];
66 -> 26;

67 [label="EVAL with clause\nappend(nil, X47, X47).\nand substitutionT19 -> nil,\nT17 -> T26,\nX47 -> cons(T26, nil),\nX40 -> cons(T26, nil)", fontsize=14, style = filled, fillcolor = lightblue];
25 -> 67 [arrowhead = none ];
67 -> 27;

68 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
25 -> 68 [arrowhead = none ];
68 -> 28;

69 [label="EVAL with clause\nappend(cons(X58, X59), X60, cons(X58, X61)) :- append(X59, X60, X61).\nand substitutionX58 -> T33,\nX59 -> T34,\nT19 -> cons(T33, T34),\nT17 -> T35,\nX60 -> cons(T35, nil),\nX61 -> X62,\nX40 -> cons(T33, X62)", fontsize=14, style = filled, fillcolor = lightblue];
26 -> 69 [arrowhead = none ];
69 -> 30;

70 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
26 -> 70 [arrowhead = none ];
70 -> 31;

71 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
27 -> 71 [arrowhead = none ];
71 -> 29;

72 [label="INSTANCE with matching:\nT19 -> T34\nT17 -> T35\nX40 -> X62", fontsize=14, style = filled, fillcolor = lightgrey];
30 -> 72 [arrowhead = none , style=dashed];
72 -> 23[style=dashed];

73 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
32 -> 73 [arrowhead = none ];
73 -> 33;

74 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
32 -> 74 [arrowhead = none ];
74 -> 34;

75 [label="EVAL with clause\nshuffle(nil, nil).\nand substitutionT7 -> nil,\nX21 -> nil", fontsize=14, style = filled, fillcolor = lightblue];
33 -> 75 [arrowhead = none ];
75 -> 35;

76 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
33 -> 76 [arrowhead = none ];
76 -> 36;

77 [label="EVAL with clause\nshuffle(cons(X74, X75), cons(X74, X76)) :- ','(reverse(X75, X77), shuffle(X77, X76)).\nand substitutionX74 -> T42,\nX75 -> T43,\nT7 -> cons(T42, T43),\nX76 -> X78,\nX21 -> cons(T42, X78)", fontsize=14, style = filled, fillcolor = lightblue];
34 -> 77 [arrowhead = none ];
77 -> 38;

78 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
34 -> 78 [arrowhead = none ];
78 -> 39;

79 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
35 -> 79 [arrowhead = none ];
79 -> 37;

80 [label="INSTANCE with matching:\nT6 -> T43\nX19 -> X77\nX21 -> X78", fontsize=14, style = filled, fillcolor = lightgrey];
38 -> 80 [arrowhead = none , style=dashed];
80 -> 6[style=dashed];

}

(2) Obligation:

Triples:

reverseA(cons(X1, X2), X3) :- reverseA(X2, X4).
reverseA(cons(X1, X2), X3) :- ','(reversecA(X2, X4), appendB(X4, X1, X3)).
appendB(cons(X1, X2), X3, cons(X1, X4)) :- appendB(X2, X3, X4).
pC(X1, X2, X3) :- reverseA(X1, X2).
pC(X1, cons(X2, X3), cons(X2, X4)) :- ','(reversecA(X1, cons(X2, X3)), pC(X3, X5, X4)).
queryD(X1) :- pC(X1, X2, X3).

Clauses:

reversecA(nil, nil).
reversecA(cons(X1, nil), cons(X1, nil)).
reversecA(cons(X1, X2), X3) :- ','(reversecA(X2, X4), appendcB(X4, X1, X3)).
appendcB(nil, X1, cons(X1, nil)).
appendcB(cons(X1, X2), X3, cons(X1, X4)) :- appendcB(X2, X3, X4).
qcC(X1, nil, nil) :- reversecA(X1, nil).
qcC(X1, cons(X2, X3), cons(X2, X4)) :- ','(reversecA(X1, cons(X2, X3)), qcC(X3, X5, X4)).

Afs:

queryD(x1)  =  queryD(x1)

(3) TriplesToPiDPProof (SOUND transformation)

We use the technique of [DT09]. With regard to the inferred argument filtering the predicates were used in the following modes:
queryD_in: (b)
pC_in: (b,f,f)
reverseA_in: (b,f)
reversecA_in: (b,f)
appendcB_in: (b,f,f)
appendB_in: (b,f,f)
Transforming TRIPLES into the following Term Rewriting System:
Pi DP problem:
The TRS P consists of the following rules:

QUERYD_IN_G(X1) → U8_G(X1, pC_in_gaa(X1, X2, X3))
QUERYD_IN_G(X1) → PC_IN_GAA(X1, X2, X3)
PC_IN_GAA(X1, X2, X3) → U5_GAA(X1, X2, X3, reverseA_in_ga(X1, X2))
PC_IN_GAA(X1, X2, X3) → REVERSEA_IN_GA(X1, X2)
REVERSEA_IN_GA(cons(X1, X2), X3) → U1_GA(X1, X2, X3, reverseA_in_ga(X2, X4))
REVERSEA_IN_GA(cons(X1, X2), X3) → REVERSEA_IN_GA(X2, X4)
REVERSEA_IN_GA(cons(X1, X2), X3) → U2_GA(X1, X2, X3, reversecA_in_ga(X2, X4))
U2_GA(X1, X2, X3, reversecA_out_ga(X2, X4)) → U3_GA(X1, X2, X3, appendB_in_gaa(X4, X1, X3))
U2_GA(X1, X2, X3, reversecA_out_ga(X2, X4)) → APPENDB_IN_GAA(X4, X1, X3)
APPENDB_IN_GAA(cons(X1, X2), X3, cons(X1, X4)) → U4_GAA(X1, X2, X3, X4, appendB_in_gaa(X2, X3, X4))
APPENDB_IN_GAA(cons(X1, X2), X3, cons(X1, X4)) → APPENDB_IN_GAA(X2, X3, X4)
PC_IN_GAA(X1, cons(X2, X3), cons(X2, X4)) → U6_GAA(X1, X2, X3, X4, reversecA_in_ga(X1, cons(X2, X3)))
U6_GAA(X1, X2, X3, X4, reversecA_out_ga(X1, cons(X2, X3))) → U7_GAA(X1, X2, X3, X4, pC_in_gaa(X3, X5, X4))
U6_GAA(X1, X2, X3, X4, reversecA_out_ga(X1, cons(X2, X3))) → PC_IN_GAA(X3, X5, X4)

The TRS R consists of the following rules:

reversecA_in_ga(nil, nil) → reversecA_out_ga(nil, nil)
reversecA_in_ga(cons(X1, nil), cons(X1, nil)) → reversecA_out_ga(cons(X1, nil), cons(X1, nil))
reversecA_in_ga(cons(X1, X2), X3) → U10_ga(X1, X2, X3, reversecA_in_ga(X2, X4))
U10_ga(X1, X2, X3, reversecA_out_ga(X2, X4)) → U11_ga(X1, X2, X3, appendcB_in_gaa(X4, X1, X3))
appendcB_in_gaa(nil, X1, cons(X1, nil)) → appendcB_out_gaa(nil, X1, cons(X1, nil))
appendcB_in_gaa(cons(X1, X2), X3, cons(X1, X4)) → U12_gaa(X1, X2, X3, X4, appendcB_in_gaa(X2, X3, X4))
U12_gaa(X1, X2, X3, X4, appendcB_out_gaa(X2, X3, X4)) → appendcB_out_gaa(cons(X1, X2), X3, cons(X1, X4))
U11_ga(X1, X2, X3, appendcB_out_gaa(X4, X1, X3)) → reversecA_out_ga(cons(X1, X2), X3)

The argument filtering Pi contains the following mapping:
pC_in_gaa(x1, x2, x3)  =  pC_in_gaa(x1)
reverseA_in_ga(x1, x2)  =  reverseA_in_ga(x1)
cons(x1, x2)  =  cons(x2)
reversecA_in_ga(x1, x2)  =  reversecA_in_ga(x1)
nil  =  nil
reversecA_out_ga(x1, x2)  =  reversecA_out_ga(x1, x2)
U10_ga(x1, x2, x3, x4)  =  U10_ga(x2, x4)
U11_ga(x1, x2, x3, x4)  =  U11_ga(x2, x4)
appendcB_in_gaa(x1, x2, x3)  =  appendcB_in_gaa(x1)
appendcB_out_gaa(x1, x2, x3)  =  appendcB_out_gaa(x1, x3)
U12_gaa(x1, x2, x3, x4, x5)  =  U12_gaa(x2, x5)
appendB_in_gaa(x1, x2, x3)  =  appendB_in_gaa(x1)
QUERYD_IN_G(x1)  =  QUERYD_IN_G(x1)
U8_G(x1, x2)  =  U8_G(x1, x2)
PC_IN_GAA(x1, x2, x3)  =  PC_IN_GAA(x1)
U5_GAA(x1, x2, x3, x4)  =  U5_GAA(x1, x4)
REVERSEA_IN_GA(x1, x2)  =  REVERSEA_IN_GA(x1)
U1_GA(x1, x2, x3, x4)  =  U1_GA(x2, x4)
U2_GA(x1, x2, x3, x4)  =  U2_GA(x2, x4)
U3_GA(x1, x2, x3, x4)  =  U3_GA(x2, x4)
APPENDB_IN_GAA(x1, x2, x3)  =  APPENDB_IN_GAA(x1)
U4_GAA(x1, x2, x3, x4, x5)  =  U4_GAA(x2, x5)
U6_GAA(x1, x2, x3, x4, x5)  =  U6_GAA(x1, x5)
U7_GAA(x1, x2, x3, x4, x5)  =  U7_GAA(x1, x5)

We have to consider all (P,R,Pi)-chains

Infinitary Constructor Rewriting Termination of PiDP implies Termination of TRIPLES

(4) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

QUERYD_IN_G(X1) → U8_G(X1, pC_in_gaa(X1, X2, X3))
QUERYD_IN_G(X1) → PC_IN_GAA(X1, X2, X3)
PC_IN_GAA(X1, X2, X3) → U5_GAA(X1, X2, X3, reverseA_in_ga(X1, X2))
PC_IN_GAA(X1, X2, X3) → REVERSEA_IN_GA(X1, X2)
REVERSEA_IN_GA(cons(X1, X2), X3) → U1_GA(X1, X2, X3, reverseA_in_ga(X2, X4))
REVERSEA_IN_GA(cons(X1, X2), X3) → REVERSEA_IN_GA(X2, X4)
REVERSEA_IN_GA(cons(X1, X2), X3) → U2_GA(X1, X2, X3, reversecA_in_ga(X2, X4))
U2_GA(X1, X2, X3, reversecA_out_ga(X2, X4)) → U3_GA(X1, X2, X3, appendB_in_gaa(X4, X1, X3))
U2_GA(X1, X2, X3, reversecA_out_ga(X2, X4)) → APPENDB_IN_GAA(X4, X1, X3)
APPENDB_IN_GAA(cons(X1, X2), X3, cons(X1, X4)) → U4_GAA(X1, X2, X3, X4, appendB_in_gaa(X2, X3, X4))
APPENDB_IN_GAA(cons(X1, X2), X3, cons(X1, X4)) → APPENDB_IN_GAA(X2, X3, X4)
PC_IN_GAA(X1, cons(X2, X3), cons(X2, X4)) → U6_GAA(X1, X2, X3, X4, reversecA_in_ga(X1, cons(X2, X3)))
U6_GAA(X1, X2, X3, X4, reversecA_out_ga(X1, cons(X2, X3))) → U7_GAA(X1, X2, X3, X4, pC_in_gaa(X3, X5, X4))
U6_GAA(X1, X2, X3, X4, reversecA_out_ga(X1, cons(X2, X3))) → PC_IN_GAA(X3, X5, X4)

The TRS R consists of the following rules:

reversecA_in_ga(nil, nil) → reversecA_out_ga(nil, nil)
reversecA_in_ga(cons(X1, nil), cons(X1, nil)) → reversecA_out_ga(cons(X1, nil), cons(X1, nil))
reversecA_in_ga(cons(X1, X2), X3) → U10_ga(X1, X2, X3, reversecA_in_ga(X2, X4))
U10_ga(X1, X2, X3, reversecA_out_ga(X2, X4)) → U11_ga(X1, X2, X3, appendcB_in_gaa(X4, X1, X3))
appendcB_in_gaa(nil, X1, cons(X1, nil)) → appendcB_out_gaa(nil, X1, cons(X1, nil))
appendcB_in_gaa(cons(X1, X2), X3, cons(X1, X4)) → U12_gaa(X1, X2, X3, X4, appendcB_in_gaa(X2, X3, X4))
U12_gaa(X1, X2, X3, X4, appendcB_out_gaa(X2, X3, X4)) → appendcB_out_gaa(cons(X1, X2), X3, cons(X1, X4))
U11_ga(X1, X2, X3, appendcB_out_gaa(X4, X1, X3)) → reversecA_out_ga(cons(X1, X2), X3)

The argument filtering Pi contains the following mapping:
pC_in_gaa(x1, x2, x3)  =  pC_in_gaa(x1)
reverseA_in_ga(x1, x2)  =  reverseA_in_ga(x1)
cons(x1, x2)  =  cons(x2)
reversecA_in_ga(x1, x2)  =  reversecA_in_ga(x1)
nil  =  nil
reversecA_out_ga(x1, x2)  =  reversecA_out_ga(x1, x2)
U10_ga(x1, x2, x3, x4)  =  U10_ga(x2, x4)
U11_ga(x1, x2, x3, x4)  =  U11_ga(x2, x4)
appendcB_in_gaa(x1, x2, x3)  =  appendcB_in_gaa(x1)
appendcB_out_gaa(x1, x2, x3)  =  appendcB_out_gaa(x1, x3)
U12_gaa(x1, x2, x3, x4, x5)  =  U12_gaa(x2, x5)
appendB_in_gaa(x1, x2, x3)  =  appendB_in_gaa(x1)
QUERYD_IN_G(x1)  =  QUERYD_IN_G(x1)
U8_G(x1, x2)  =  U8_G(x1, x2)
PC_IN_GAA(x1, x2, x3)  =  PC_IN_GAA(x1)
U5_GAA(x1, x2, x3, x4)  =  U5_GAA(x1, x4)
REVERSEA_IN_GA(x1, x2)  =  REVERSEA_IN_GA(x1)
U1_GA(x1, x2, x3, x4)  =  U1_GA(x2, x4)
U2_GA(x1, x2, x3, x4)  =  U2_GA(x2, x4)
U3_GA(x1, x2, x3, x4)  =  U3_GA(x2, x4)
APPENDB_IN_GAA(x1, x2, x3)  =  APPENDB_IN_GAA(x1)
U4_GAA(x1, x2, x3, x4, x5)  =  U4_GAA(x2, x5)
U6_GAA(x1, x2, x3, x4, x5)  =  U6_GAA(x1, x5)
U7_GAA(x1, x2, x3, x4, x5)  =  U7_GAA(x1, x5)

We have to consider all (P,R,Pi)-chains

(5) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LOPSTR] contains 3 SCCs with 10 less nodes.

(6) Complex Obligation (AND)

(7) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

APPENDB_IN_GAA(cons(X1, X2), X3, cons(X1, X4)) → APPENDB_IN_GAA(X2, X3, X4)

The TRS R consists of the following rules:

reversecA_in_ga(nil, nil) → reversecA_out_ga(nil, nil)
reversecA_in_ga(cons(X1, nil), cons(X1, nil)) → reversecA_out_ga(cons(X1, nil), cons(X1, nil))
reversecA_in_ga(cons(X1, X2), X3) → U10_ga(X1, X2, X3, reversecA_in_ga(X2, X4))
U10_ga(X1, X2, X3, reversecA_out_ga(X2, X4)) → U11_ga(X1, X2, X3, appendcB_in_gaa(X4, X1, X3))
appendcB_in_gaa(nil, X1, cons(X1, nil)) → appendcB_out_gaa(nil, X1, cons(X1, nil))
appendcB_in_gaa(cons(X1, X2), X3, cons(X1, X4)) → U12_gaa(X1, X2, X3, X4, appendcB_in_gaa(X2, X3, X4))
U12_gaa(X1, X2, X3, X4, appendcB_out_gaa(X2, X3, X4)) → appendcB_out_gaa(cons(X1, X2), X3, cons(X1, X4))
U11_ga(X1, X2, X3, appendcB_out_gaa(X4, X1, X3)) → reversecA_out_ga(cons(X1, X2), X3)

The argument filtering Pi contains the following mapping:
cons(x1, x2)  =  cons(x2)
reversecA_in_ga(x1, x2)  =  reversecA_in_ga(x1)
nil  =  nil
reversecA_out_ga(x1, x2)  =  reversecA_out_ga(x1, x2)
U10_ga(x1, x2, x3, x4)  =  U10_ga(x2, x4)
U11_ga(x1, x2, x3, x4)  =  U11_ga(x2, x4)
appendcB_in_gaa(x1, x2, x3)  =  appendcB_in_gaa(x1)
appendcB_out_gaa(x1, x2, x3)  =  appendcB_out_gaa(x1, x3)
U12_gaa(x1, x2, x3, x4, x5)  =  U12_gaa(x2, x5)
APPENDB_IN_GAA(x1, x2, x3)  =  APPENDB_IN_GAA(x1)

We have to consider all (P,R,Pi)-chains

(8) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(9) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

APPENDB_IN_GAA(cons(X1, X2), X3, cons(X1, X4)) → APPENDB_IN_GAA(X2, X3, X4)

R is empty.
The argument filtering Pi contains the following mapping:
cons(x1, x2)  =  cons(x2)
APPENDB_IN_GAA(x1, x2, x3)  =  APPENDB_IN_GAA(x1)

We have to consider all (P,R,Pi)-chains

(10) PiDPToQDPProof (SOUND transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(11) Obligation:

Q DP problem:
The TRS P consists of the following rules:

APPENDB_IN_GAA(cons(X2)) → APPENDB_IN_GAA(X2)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.

(12) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

• APPENDB_IN_GAA(cons(X2)) → APPENDB_IN_GAA(X2)
  The graph contains the following edges 1 > 1

(13) YES

(14) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

REVERSEA_IN_GA(cons(X1, X2), X3) → REVERSEA_IN_GA(X2, X4)

The TRS R consists of the following rules:

reversecA_in_ga(nil, nil) → reversecA_out_ga(nil, nil)
reversecA_in_ga(cons(X1, nil), cons(X1, nil)) → reversecA_out_ga(cons(X1, nil), cons(X1, nil))
reversecA_in_ga(cons(X1, X2), X3) → U10_ga(X1, X2, X3, reversecA_in_ga(X2, X4))
U10_ga(X1, X2, X3, reversecA_out_ga(X2, X4)) → U11_ga(X1, X2, X3, appendcB_in_gaa(X4, X1, X3))
appendcB_in_gaa(nil, X1, cons(X1, nil)) → appendcB_out_gaa(nil, X1, cons(X1, nil))
appendcB_in_gaa(cons(X1, X2), X3, cons(X1, X4)) → U12_gaa(X1, X2, X3, X4, appendcB_in_gaa(X2, X3, X4))
U12_gaa(X1, X2, X3, X4, appendcB_out_gaa(X2, X3, X4)) → appendcB_out_gaa(cons(X1, X2), X3, cons(X1, X4))
U11_ga(X1, X2, X3, appendcB_out_gaa(X4, X1, X3)) → reversecA_out_ga(cons(X1, X2), X3)

The argument filtering Pi contains the following mapping:
cons(x1, x2)  =  cons(x2)
reversecA_in_ga(x1, x2)  =  reversecA_in_ga(x1)
nil  =  nil
reversecA_out_ga(x1, x2)  =  reversecA_out_ga(x1, x2)
U10_ga(x1, x2, x3, x4)  =  U10_ga(x2, x4)
U11_ga(x1, x2, x3, x4)  =  U11_ga(x2, x4)
appendcB_in_gaa(x1, x2, x3)  =  appendcB_in_gaa(x1)
appendcB_out_gaa(x1, x2, x3)  =  appendcB_out_gaa(x1, x3)
U12_gaa(x1, x2, x3, x4, x5)  =  U12_gaa(x2, x5)
REVERSEA_IN_GA(x1, x2)  =  REVERSEA_IN_GA(x1)

We have to consider all (P,R,Pi)-chains

(15) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(16) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

REVERSEA_IN_GA(cons(X1, X2), X3) → REVERSEA_IN_GA(X2, X4)

R is empty.
The argument filtering Pi contains the following mapping:
cons(x1, x2)  =  cons(x2)
REVERSEA_IN_GA(x1, x2)  =  REVERSEA_IN_GA(x1)

We have to consider all (P,R,Pi)-chains

(17) PiDPToQDPProof (SOUND transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(18) Obligation:

Q DP problem:
The TRS P consists of the following rules:

REVERSEA_IN_GA(cons(X2)) → REVERSEA_IN_GA(X2)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.

(19) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

• REVERSEA_IN_GA(cons(X2)) → REVERSEA_IN_GA(X2)
  The graph contains the following edges 1 > 1

(20) YES

(21) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

PC_IN_GAA(X1, cons(X2, X3), cons(X2, X4)) → U6_GAA(X1, X2, X3, X4, reversecA_in_ga(X1, cons(X2, X3)))
U6_GAA(X1, X2, X3, X4, reversecA_out_ga(X1, cons(X2, X3))) → PC_IN_GAA(X3, X5, X4)

The TRS R consists of the following rules:

reversecA_in_ga(nil, nil) → reversecA_out_ga(nil, nil)
reversecA_in_ga(cons(X1, nil), cons(X1, nil)) → reversecA_out_ga(cons(X1, nil), cons(X1, nil))
reversecA_in_ga(cons(X1, X2), X3) → U10_ga(X1, X2, X3, reversecA_in_ga(X2, X4))
U10_ga(X1, X2, X3, reversecA_out_ga(X2, X4)) → U11_ga(X1, X2, X3, appendcB_in_gaa(X4, X1, X3))
appendcB_in_gaa(nil, X1, cons(X1, nil)) → appendcB_out_gaa(nil, X1, cons(X1, nil))
appendcB_in_gaa(cons(X1, X2), X3, cons(X1, X4)) → U12_gaa(X1, X2, X3, X4, appendcB_in_gaa(X2, X3, X4))
U12_gaa(X1, X2, X3, X4, appendcB_out_gaa(X2, X3, X4)) → appendcB_out_gaa(cons(X1, X2), X3, cons(X1, X4))
U11_ga(X1, X2, X3, appendcB_out_gaa(X4, X1, X3)) → reversecA_out_ga(cons(X1, X2), X3)

The argument filtering Pi contains the following mapping:
cons(x1, x2)  =  cons(x2)
reversecA_in_ga(x1, x2)  =  reversecA_in_ga(x1)
nil  =  nil
reversecA_out_ga(x1, x2)  =  reversecA_out_ga(x1, x2)
U10_ga(x1, x2, x3, x4)  =  U10_ga(x2, x4)
U11_ga(x1, x2, x3, x4)  =  U11_ga(x2, x4)
appendcB_in_gaa(x1, x2, x3)  =  appendcB_in_gaa(x1)
appendcB_out_gaa(x1, x2, x3)  =  appendcB_out_gaa(x1, x3)
U12_gaa(x1, x2, x3, x4, x5)  =  U12_gaa(x2, x5)
PC_IN_GAA(x1, x2, x3)  =  PC_IN_GAA(x1)
U6_GAA(x1, x2, x3, x4, x5)  =  U6_GAA(x1, x5)

We have to consider all (P,R,Pi)-chains

(22) PiDPToQDPProof (SOUND transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(23) Obligation:

Q DP problem:
The TRS P consists of the following rules:

PC_IN_GAA(X1) → U6_GAA(X1, reversecA_in_ga(X1))
U6_GAA(X1, reversecA_out_ga(X1, cons(X3))) → PC_IN_GAA(X3)

The TRS R consists of the following rules:

reversecA_in_ga(nil) → reversecA_out_ga(nil, nil)
reversecA_in_ga(cons(nil)) → reversecA_out_ga(cons(nil), cons(nil))
reversecA_in_ga(cons(X2)) → U10_ga(X2, reversecA_in_ga(X2))
U10_ga(X2, reversecA_out_ga(X2, X4)) → U11_ga(X2, appendcB_in_gaa(X4))
appendcB_in_gaa(nil) → appendcB_out_gaa(nil, cons(nil))
appendcB_in_gaa(cons(X2)) → U12_gaa(X2, appendcB_in_gaa(X2))
U12_gaa(X2, appendcB_out_gaa(X2, X4)) → appendcB_out_gaa(cons(X2), cons(X4))
U11_ga(X2, appendcB_out_gaa(X4, X3)) → reversecA_out_ga(cons(X2), X3)

The set Q consists of the following terms:

reversecA_in_ga(x0)
U10_ga(x0, x1)
appendcB_in_gaa(x0)
U12_gaa(x0, x1)
U11_ga(x0, x1)

We have to consider all (P,Q,R)-chains.

(24) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04,JAR06].

The following pairs can be oriented strictly and are deleted.

PC_IN_GAA(X1) → U6_GAA(X1, reversecA_in_ga(X1))

The remaining pairs can at least be oriented weakly.
Used ordering: Polynomial interpretation [POLO]:

POL(PC_IN_GAA(x₁)) = 1 + x₁   
POL(U10_ga(x₁, x₂)) = 1 + x₂   
POL(U11_ga(x₁, x₂)) = x₂   
POL(U12_gaa(x₁, x₂)) = 1 + x₂   
POL(U6_GAA(x₁, x₂)) = x₂   
POL(appendcB_in_gaa(x₁)) = 1 + x₁   
POL(appendcB_out_gaa(x₁, x₂)) = x₂   
POL(cons(x₁)) = 1 + x₁   
POL(nil) = 0   
POL(reversecA_in_ga(x₁)) = x₁   
POL(reversecA_out_ga(x₁, x₂)) = x₂   

The following usable rules [FROCOS05] with respect to the argument filtering of the ordering [JAR06] were oriented:

reversecA_in_ga(nil) → reversecA_out_ga(nil, nil)
reversecA_in_ga(cons(nil)) → reversecA_out_ga(cons(nil), cons(nil))
reversecA_in_ga(cons(X2)) → U10_ga(X2, reversecA_in_ga(X2))
U10_ga(X2, reversecA_out_ga(X2, X4)) → U11_ga(X2, appendcB_in_gaa(X4))
appendcB_in_gaa(nil) → appendcB_out_gaa(nil, cons(nil))
appendcB_in_gaa(cons(X2)) → U12_gaa(X2, appendcB_in_gaa(X2))
U11_ga(X2, appendcB_out_gaa(X4, X3)) → reversecA_out_ga(cons(X2), X3)
U12_gaa(X2, appendcB_out_gaa(X2, X4)) → appendcB_out_gaa(cons(X2), cons(X4))

(25) Obligation:

Q DP problem:
The TRS P consists of the following rules:

U6_GAA(X1, reversecA_out_ga(X1, cons(X3))) → PC_IN_GAA(X3)

The TRS R consists of the following rules:

reversecA_in_ga(nil) → reversecA_out_ga(nil, nil)
reversecA_in_ga(cons(nil)) → reversecA_out_ga(cons(nil), cons(nil))
reversecA_in_ga(cons(X2)) → U10_ga(X2, reversecA_in_ga(X2))
U10_ga(X2, reversecA_out_ga(X2, X4)) → U11_ga(X2, appendcB_in_gaa(X4))
appendcB_in_gaa(nil) → appendcB_out_gaa(nil, cons(nil))
appendcB_in_gaa(cons(X2)) → U12_gaa(X2, appendcB_in_gaa(X2))
U12_gaa(X2, appendcB_out_gaa(X2, X4)) → appendcB_out_gaa(cons(X2), cons(X4))
U11_ga(X2, appendcB_out_gaa(X4, X3)) → reversecA_out_ga(cons(X2), X3)

The set Q consists of the following terms:

reversecA_in_ga(x0)
U10_ga(x0, x1)
appendcB_in_gaa(x0)
U12_gaa(x0, x1)
U11_ga(x0, x1)

We have to consider all (P,Q,R)-chains.

(26) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 0 SCCs with 1 less node.

(27) TRUE